fifo+send(es;C;in;m;req;j;i;e)
== (isrcv(e)) & lnk(e) = in(j) & ((tag(e) = m)  (tag(e) = req)) & (i  val(e).1) 

latex

---

clarification:

fifo+send(es;C;in;m;req;j;i;e)
== (es-isrcv(es; e))
== & es-lnk(es; e) = in(j)  IdLnk
== & ((es-tag(es; e) = m  Id)  (es-tag(es; e) = req  Id))
== & (i  es-val(es; e).1  C) 

latex

Definitions	b, isrcv(e), IdLnk, lnk(e), f(a), P & Q, P  Q, s = t, Id, tag(e), (x  l), t.1, val(e)
FDL editor aliases	fifo+send